$\forall$$T$:Type, $x$:$T$, $a$:Atom1. AtomFree(Type;$T$) $\Rightarrow$ AtomFree($T$;$x$) $\Rightarrow$ $x$:$T$$>>$$a$ $\Rightarrow$ False